open import Data.Nat
open import Data.Vec
open import Relation.Binary.Core
open import Algebra.Structures
open import Algebra
open import Agda.Builtin.Unit
open import Data.Empty
open import Relation.Nullary
open import Data.Nat renaming (_⊔_ to _ℕ⊔_ ; _+_ to _ℕ+_; _*_ to _ℕ*_ ; _≟_ to _ℕ≟_)
open import Data.Product
open import Data.Nat.Properties 
open import Data.Bool renaming ( _≟_ to _B≟_)
open import Agda.Builtin.Equality
open import Relation.Binary.PropositionalEquality
open import Data.Bool.Properties
open import Function.Equivalence
open import Function.Equality
open import Function renaming (_∘_ to _∘ₕ_)
import Agda.Primitive
import Data.Fin 
import Data.Integer as Int

module UnivariatePolynomial {a b} (cRing : CommutativeRing a b) (_coeff≟_ : Decidable (CommutativeRing._≈_ cRing)) where
open CommutativeRing cRing

IsUnivPoly : {n : ℕ} → (poly : Vec Carrier n) → Bool
IsUnivPoly [] = true
IsUnivPoly (x ∷ poly) with x coeff≟ 0#
... | yes p = false
... | no ¬p = true

private
  IUH : {n : ℕ} → (x : Carrier) → (p : Vec Carrier n) → (qqq : (x ≈ 0#) → ⊥ ) → T (IsUnivPoly (x ∷ p))
  IUH x p qqq with x coeff≟ 0#
  IUH x p qqq | yes p₁ = qqq p₁
  IUH x p qqq | no ¬p = tt

IsMonic : {n : ℕ} → (poly : Vec Carrier n) → {_ : T (IsUnivPoly poly)}→ Set
IsMonic [] = ⊥
IsMonic (x ∷ poly) with x coeff≟ 1#
... | yes p = ⊤
... | no ¬p = ⊥

record SomePoly : Set a where
  constructor xD
  field
    n : ℕ
    p : Vec Carrier n
    m : ℕ
    n≤m : n ≤ m
    isPoly : T(IsUnivPoly p)

fromPoly : {n : ℕ} → (p : Vec Carrier n) → (isPoly : T (IsUnivPoly p)) → SomePoly
fromPoly {n} p isPoly = xD n p n ≤-refl isPoly

fromAbomination : {n : ℕ} → Σ ℕ (λ m → ((m ≤′ n) × (Σ (Vec Carrier m) (λ p → T (IsUnivPoly p))))) → SomePoly
fromAbomination {n} p = xD (proj₁ p) (proj₁ $ proj₂ $ proj₂ $ p) n (≤′⇒≤ $ proj₁ $ proj₂ $ p) (proj₂ $ proj₂ $ proj₂ $ p)

private
  EqualPolys- : {n : ℕ } → (p1 p2 : Vec Carrier n) → Bool
  EqualPolys- [] [] = true
  EqualPolys- (x ∷ p1) (y ∷ p2) with x coeff≟ y
  ... | (yes _) = true ∧ (EqualPolys- p1 p2)
  ... | (no _) = false

EqualPolys : {n m : ℕ } → (n ≡ m) → (p1 : Vec Carrier n) → (p2 : Vec Carrier m)
  → {_ : T (IsUnivPoly p1 )} → {_ : T (IsUnivPoly p2)} → Bool
EqualPolys {n} {n}  _≡_.refl p1 p2 = EqualPolys- p1 p2

eqPolys : (p1 p2 : SomePoly) → Bool
eqPolys p1 p2 with (SomePoly.n p1) ℕ≟ (SomePoly.n p2) 
eqPolys p1 p2 | yes proof = (EqualPolys proof (p1. p) (p2. p) {p1. isPoly} {p2. isPoly}) where open SomePoly
eqPolys p1 p2 | no ¬p = false

toJesTrochęDziwne : {n : ℕ} → (p : Vec Carrier n) → (IsUnivPoly p) ≡ true → T (IsUnivPoly p)
toJesTrochęDziwne p proof = Function.Equivalence.Equivalence.from (T-≡ {(IsUnivPoly p)}) ⟨$⟩ proof

toJesTrochęDziwne2 : {n : ℕ} → (p : Vec Carrier n) → T (IsUnivPoly p) → (IsUnivPoly p) ≡ true
toJesTrochęDziwne2 p proof =  Function.Equivalence.Equivalence.to (T-≡ {(IsUnivPoly p)}) ⟨$⟩ proof

private
  revAddHelper : {n m : ℕ} → (p1 : Vec Carrier n) → (p2 : Vec Carrier m) → Vec Carrier (n ℕ⊔ m)
  revAddHelper [] p2 = p2
  revAddHelper (x ∷ p1) [] = x ∷ p1
  revAddHelper (x ∷ p1) (y ∷ p2) = Algebra.CommutativeRing._+_ cRing x y  ∷ (revAddHelper p1 p2)
  stripZeros : {n : ℕ} → (p : Vec Carrier n) → Σ ℕ λ m → ((m ≤′ n) × (Σ (Vec Carrier m) (λ p → T (IsUnivPoly p))))
  stripZeros {n} polyn with (IsUnivPoly polyn) B≟ true
  stripZeros   {.0} []  | _ = 0 , ≤′-refl , ([] , tt)  -- Ten przypadek jest konieczny żeby kompilator ogarnął że ta funkcja się wykonuje w kończonym czasie
  stripZeros {suc n} polyn@(x ∷ p) | y@(yes proof) = suc n , ≤′-refl , (polyn , Function.Equivalence.Equivalence.from T-≡ ⟨$⟩ proof)
  stripZeros {suc n} polyn@(x ∷ p) | not@(no ¬p) = let
    q = stripZeros p
    helperProof : proj₁ q ≤′ n
    helperProof = (proj₁ (proj₂ q))
    in (proj₁ q) , (≤′-step helperProof , (proj₁ (proj₂ (proj₂ q)) , (proj₂ (proj₂ (proj₂ q)))))
  spq : {n : ℕ} → (x : Carrier) → (p : Vec Carrier n) → (isPoly : T(IsUnivPoly (x ∷ p))) →
    (proj₁ $ stripZeros (x ∷ p)) ≡ (suc n) 
  spq x p isPoly with (IsUnivPoly (x ∷ p)) B≟ true
  spq x p isPoly | yes p₁ = _≡_.refl 
  spq x p isPoly | no ¬p = ⊥-elim (¬p (toJesTrochęDziwne2 (x ∷ p) (isPoly))) 
  --  stripPoly : {n : ℕ} → (p : Vec Carrier n) → (isPoly : T(IsUnivPoly p)) → T $ eqPolys (fromAbomination (stripZeros p))  (fromPoly p isPoly)
--  stripPoly [] tt = tt

addPolys : {n m : ℕ} → (p1 : Vec Carrier n) → (p2 : Vec Carrier m) → {isPoly1 : T (IsUnivPoly p1)} → {isPoly2 : T (IsUnivPoly p2)}  →
 Σ ℕ λ q → (q ≤′ (n ⊔ m) × (Σ (Vec Carrier q) (λ p → T (IsUnivPoly p))))
 -- UWAGA: to że (n ⊔ m) się tu zgadza to jest przypadek, w innych działaniach trzeba uwzględnić że dł wektora != stopień
addPolys {n} {m} p1 p2 = let
  polyWithPossiblyLeadingZeros : Vec Carrier (n ℕ⊔ m)
  polyWithPossiblyLeadingZeros = reverse (revAddHelper (reverse p1) (reverse p2))
  in stripZeros polyWithPossiblyLeadingZeros

-- multplyByX degree 1+

data PolynomialDegree : Set where
  #-1 : PolynomialDegree
  NonNeg : ℕ → PolynomialDegree

degreeToVecLen : PolynomialDegree → ℕ
degreeToVecLen #-1 = 0
degreeToVecLen (NonNeg x) = suc x

vecLenToDegree : (n : ℕ) → PolynomialDegree
vecLenToDegree 0 = #-1
vecLenToDegree (suc n) = NonNeg n

degree : {n : ℕ} → (poly : Vec Carrier n) → {isPoly : T (IsUnivPoly poly)} → PolynomialDegree
degree {n} _ = vecLenToDegree n

degSuc : PolynomialDegree → PolynomialDegree
degSuc = vecLenToDegree ∘ₕ suc ∘ₕ degreeToVecLen

degreeMax : (d1 : PolynomialDegree) → (d2 : PolynomialDegree) → PolynomialDegree
degreeMax #-1 d2 = d2
degreeMax d1 #-1 = d1
degreeMax (NonNeg x) (NonNeg y) = NonNeg (x ℕ⊔ y)

mulMaxDegree : (d1 : PolynomialDegree) → (d2 : PolynomialDegree) → PolynomialDegree
mulMaxDegree #-1 d2 = #-1
mulMaxDegree (NonNeg x) #-1 = #-1
mulMaxDegree (NonNeg x) (NonNeg y) = NonNeg (x ℕ+ y)

PolyOfDegree : (d : PolynomialDegree) → Set _
PolyOfDegree d = Vec Carrier (degreeToVecLen d)

_deg≤_ : (d1 d2 : PolynomialDegree) → Set _
d1 deg≤ d2 = (degreeToVecLen d1) ≤ (degreeToVecLen d2)

_deg≤ℕ_ : (d : PolynomialDegree) → (n : ℕ) →  Set
#-1 deg≤ℕ n = ⊤
NonNeg x deg≤ℕ n = x ≤ n

degToℤ : PolynomialDegree → Int.ℤ
degToℤ  #-1 = Int.-[1+_] 0
degToℤ (NonNeg n) = Int.+_ n

_deg≤ℤ_ : (d : PolynomialDegree) → (z : Int.ℤ) →  Set
d deg≤ℤ z = (degToℤ d) Int.≤ z

-- hacky for better normalisation :( (should be same as maxMulDegree $ degreeToVecLen)
mulMaxDegreeH : (vecLen1 : ℕ) → (vecLen2 : ℕ) → ℕ
mulMaxDegreeH 0 vecLen2 = 0
mulMaxDegreeH vecLen1 0 = 0
mulMaxDegreeH (suc vecLen1) (suc vecLen2) = suc (vecLen1 ℕ+ vecLen2)

nonEmptyPoly : {n : ℕ} → (poly : Vec Carrier n) → {isPoly : T (IsUnivPoly poly)} → Bool -- to samo można wyrazić `degree` ale boje się o normalizację
nonEmptyPoly [] = false
nonEmptyPoly (x ∷ p ) = true

#-1NotSuc : {d : PolynomialDegree} → #-1 ≡ (degSuc d) → ⊥
#-1NotSuc {#-1}  = λ ()
#-1NotSuc {NonNeg x} = λ ()

coeffOfPower : {d : ℕ} → (n : ℕ) →
  (p : Vec Carrier d) → {_ : T (IsUnivPoly p)} → Carrier
coeffOfPower {d} n p with d >? n
coeffOfPower {d} n p | yes proof = lookup (reverse p) (Data.Fin.fromℕ≤ proof)
coeffOfPower {d} n p | no ¬p = 0#

-- Uwaga do mnożenia: W pierścieniu a * b może się równać 0 albo 1 (np pierścień liczb całkowitych modulo 4)
UnivNonEmptyPoly : {n : ℕ} → (poly : Vec Carrier (suc n)) → (head poly ≈ 0# → ⊥) → T (IsUnivPoly poly)
UnivNonEmptyPoly (x ∷ p) proof with x coeff≟ 0#
... | (yes oops) = proof oops
... | (no _) = tt

private
  addZeroAtEnd : {m : ℕ} → Vec Carrier m → Vec Carrier (suc m)
  addZeroAtEnd = λ { [] → 0# ∷ [] ; (x ∷ p) → x ∷ (addZeroAtEnd p) }
multiplyNonEmptyPolyByX : {a : ℕ} → (poly : Vec Carrier (suc a)) → {isPoly : T (IsUnivPoly poly)} →
  Σ (Vec Carrier (suc (suc a))) (λ p → T (IsUnivPoly p))
multiplyNonEmptyPolyByX (x ∷ p) {isPoly} with x coeff≟ 0#
... | (yes oops) = ⊥-elim isPoly
... | (no proof') =  (addZeroAtEnd (x ∷ p)) , UnivNonEmptyPoly (addZeroAtEnd (x ∷ p)) proof'

multiplyByX : {a : ℕ} → (poly : Vec Carrier a) → {isPoly : T (IsUnivPoly poly)} →
  Σ ℕ (λ q → (q ≤′ (suc a)   × Σ (Vec Carrier q) (λ p → T (IsUnivPoly p))))
multiplyByX []  = 0 , (≤′-step ≤′-refl) , [] , tt
multiplyByX {suc n}(x ∷ p) {isPoly} =  suc (suc n) , (≤′-refl , multiplyNonEmptyPolyByX (x ∷ p) {isPoly})



multiplyByScalar : {n : ℕ} → (p : Vec Carrier n) → {isPoly : T (IsUnivPoly p)} → (scalar : Carrier) → 
 Σ ℕ λ q → (q ≤′ (mulMaxDegreeH 1 n) × (Σ (Vec Carrier q) (λ p → T (IsUnivPoly p))))
multiplyByScalar [] s = 0 , (≤′-refl , ([] , tt))
multiplyByScalar {suc n} (x ∷ p) s = stripZeros (Data.Vec.map (λ c → Algebra.CommutativeRing._*_ cRing c s) ((x ∷ p)))


private
  h1 : (n m : ℕ) → (suc m) ≤′ (n ℕ+ suc m)
  h1 ℕ.zero m = ≤′-refl
  h1 (suc n) m = ≤′-step (h1 n m)
  helper1234 : ( n m  : ℕ) →  (n ℕ+ suc m)  ⊔ suc m ≡ n ℕ+ suc m
  helper1234 n m = (m≤n⇒n⊔m≡n {suc m}  {n ℕ+ suc m} (≤′⇒≤ (h1 n m)))
  tq : (n m : ℕ ) → (n ℕ+ suc m)  ≤ (suc (n ℕ+ m))
  tq ℕ.zero m = ≤′⇒≤ ≤′-refl
  tq (suc n) m = s≤s (tq n m)
  thm : (n m : ℕ ) → (n ℕ+ suc m) ⊔ (suc m) ≤′ (suc (n ℕ+ m)) -- to jest tak naprawdę równe
  thm n m =  ≤⇒≤′ (≤-trans (≤-reflexive (( helper1234 n m))) (tq n m))
  addUncertain : (b1 b2 bx : ℕ) → (b1 ⊔ b2 ≤′ bx)  →  Σ ℕ (λ q → q ≤′ b1 × Σ (Vec Carrier q) (λ p → T (IsUnivPoly p))) →
    Σ ℕ (λ q → q ≤′ b2 × Σ (Vec Carrier q) (λ p → T (IsUnivPoly p))) → 
    Σ ℕ (λ q → q ≤′ bx × Σ (Vec Carrier q) (λ p → T (IsUnivPoly p)))
  addUncertain b1 b2 bx neq p1 p2 = let
    added : Σ ℕ (λ q → q ≤′ proj₁ p1 ⊔ proj₁ p2 × Σ (Vec Carrier q) (λ p → T (IsUnivPoly p)))
    added = addPolys (proj₁ $ proj₂ $ proj₂ p1) (proj₁ $ proj₂ $ proj₂ p2) {proj₂ $ proj₂ $ proj₂ p1} {(proj₂ $ proj₂ $ proj₂ p2)}
    --aaa : proj₁ p1 
    newQ = proj₁ added

    f1 : proj₁ p1 ≤′ b1
    f1 = proj₁ $ proj₂ $ p1
    f2 : proj₁ p2 ≤′ b2
    f2 = proj₁ $ proj₂ $ p2
    asd : newQ ≤′ proj₁ p1 ⊔ proj₁ p2
    asd = proj₁ $ proj₂ $ added
    iCoTeraz : newQ ≤′ b1 ⊔ b2
    iCoTeraz = ≤⇒≤′ ( ≤-trans (≤′⇒≤ asd) ( ⊔-mono-≤  (≤′⇒≤ f1) (≤′⇒≤ f2)) ) 
    finish : proj₁ added ≤′ bx
    finish = ≤⇒≤′ (≤-trans (≤′⇒≤ iCoTeraz) (≤′⇒≤ neq))  -- teraz tylko p21 added < b1 u b2 < bx 
    in (proj₁ added) , (finish , ((proj₁ $ proj₂ $ proj₂ $ added) , (proj₂ $ proj₂ $ proj₂ $ added)))
  mulHelper : {n m : ℕ} → (reversedCoeffs : Vec Carrier (suc n)) → (p2 : Vec Carrier (suc m)) → (isPoly : T (IsUnivPoly p2) ) →
    Σ ℕ λ q → (q ≤′ (mulMaxDegreeH (suc n) (suc m)) × (Σ (Vec Carrier q) (λ p → T (IsUnivPoly p))))
  mulHelper {n} {m} (s ∷ []) (x ∷ polys) isPoly = multiplyByScalar (x ∷ polys) {isPoly} s
  mulHelper {n} {m} (s ∷ s2 ∷ scalars) (x ∷ polys) isPoly = let
    p2 = (x ∷ polys)
    movedP2 : Σ (Vec Carrier (suc (suc m))) (λ p → T (IsUnivPoly p)) 
    movedP2 = multiplyNonEmptyPolyByX p2 {isPoly}
    multPld : Σ ℕ (λ q → q ≤′ (n ℕ+ suc m) × Σ (Vec Carrier q) (λ p → T (IsUnivPoly p)))
    multPld = mulHelper (s2 ∷ scalars) (proj₁  movedP2) ((proj₂ $ movedP2))
    mulByScalar : Σ ℕ (λ q → q ≤′ suc m × Σ (Vec Carrier q) (λ p → T (IsUnivPoly p)))
    mulByScalar = multiplyByScalar (x ∷ polys) {isPoly} s

    added = addPolys (proj₁ $ proj₂ $ proj₂ $ multPld) (proj₁ $ proj₂ $ proj₂ $ mulByScalar)
      {(proj₂ $ proj₂ $ proj₂ $ multPld)} {(proj₂ $ proj₂ $ proj₂ $ mulByScalar)}
    addedTheOtherWay = addPolys (proj₁ $ proj₂ $ proj₂ $ mulByScalar) (proj₁ $ proj₂ $ proj₂ $ multPld)
      {(proj₂ $ proj₂ $ proj₂ $ mulByScalar)} {(proj₂ $ proj₂ $ proj₂ $ multPld)}
    result : Σ ℕ (λ q → q ≤′ (suc (n ℕ+ m)) × Σ (Vec Carrier q) (λ p → T (IsUnivPoly p)))
    result = addUncertain (n ℕ+ suc m) (suc m) ((suc (n ℕ+ m))) (thm n m)  multPld mulByScalar
    in result 

{--
Uwaga: W ogólnym przypadku deg(f(x)*g(x)) != deg(f)+deg(g)
Na przykład dla pierścienia przemiennego liczb całkowitych modulo 4:
(2x + 2)*(2) = 0
--}
multiplyPolys : {n m : ℕ} → (p1 : Vec Carrier n) → (p2 : Vec Carrier m) → {isPoly1 : T (IsUnivPoly p1)} → {isPoly2 : T (IsUnivPoly p2)}  →
 Σ ℕ λ q → (q ≤′ (mulMaxDegreeH n m) × (Σ (Vec Carrier q) (λ p → T (IsUnivPoly p))))
multiplyPolys {.0} {.0} [] [] = 0 , (≤′-refl , ([] , tt))
multiplyPolys {.0} {(suc qq)} [] (x ∷ p2) = 0 , (≤′-refl , ([] , tt))
multiplyPolys {(suc qq)} {.0} (x ∷ p1) [] = 0 , (≤′-refl , ([] , tt))
multiplyPolys {.(suc _)} {.(suc _)} (x ∷ p1) (y ∷ p2) {isPoly1 = isPoly1} {isPoly2 = isPoly2} = mulHelper (reverse (x ∷ p1)) (y ∷ p2) isPoly2 

isZeroPoly : T (IsUnivPoly [])
isZeroPoly = tt

ZeroPolyAnihilates : { n : ℕ} → (p : Vec Carrier n) → (isP : T( IsUnivPoly p)) →
 (multiplyPolys p [] {isP} {isZeroPoly}) ≡ (0 , (≤⇒≤′ z≤n) , ([] , isZeroPoly))
ZeroPolyAnihilates {.0} [] isP = _≡_.refl
ZeroPolyAnihilates {.(suc _)} (x ∷ p) isP = _≡_.refl
{--
addingPolysCommute : {n m : ℕ} → (p1 : Vec Carrier n) → (p2 : Vec Carrier m)
  → (i1 : T( IsUnivPoly p1)) → (i2 : T(IsUnivPoly p2)) → (addPolys p1 p2 {i1} {i2}) ≡ (addPolys p2 p1 {i2} {i1})
addingPolysCommute p1 p2 i1 i2 = ?
--}

private
  mulMaxDegreeH1 : (n : ℕ) → n ≤ (mulMaxDegreeH n 1)
  mulMaxDegreeH1 zero = z≤n
  mulMaxDegreeH1 (suc n) = s≤s ( ≤″⇒≤ ((less-than-or-equal {n} _≡_.refl)))
  mulMaxDegreeH1′ : (n : ℕ) → n ≤ (mulMaxDegreeH 1 n)
  mulMaxDegreeH1′ zero = z≤n
  mulMaxDegreeH1′ (suc n) = ≤′⇒≤ ≤′-refl

{--
multiplyBy1 : {n : ℕ} → (p : Vec Carrier n) → {isPoly : T (IsUnivPoly p)} →
  T $ (eqPolys (fromAbomination (multiplyByScalar p {isPoly} 1#))) (fromAbomination (n , ((≤⇒≤′ $  mulMaxDegreeH1′ n) , (p , isPoly))))
multiplyBy1 {n} [] {isPoly} =  tt
multiplyBy1 (x ∷ p) {isPoly} = {!!}
--}
{--
We say that two polynomials a and b over a commutative ring are
strongly relatively prime i f there exist polynomials s and t such that
sa + tb = 1.
--}
